Problem:
first(0(),X) -> nil()
first(s(X),cons(Y)) -> cons(Y)
from(X) -> cons(X)
Proof:
Complexity Transformation Processor:
strict:
first(0(),X) -> nil()
first(s(X),cons(Y)) -> cons(Y)
from(X) -> cons(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[from](x0) = x0 + 1,
[cons](x0) = x0,
[s](x0) = x0,
[nil] = 0,
[first](x0, x1) = x0 + x1 + 50,
[0] = 64
orientation:
first(0(),X) = X + 114 >= 0 = nil()
first(s(X),cons(Y)) = X + Y + 50 >= Y = cons(Y)
from(X) = X + 1 >= X = cons(X)
problem:
strict:
weak:
first(0(),X) -> nil()
first(s(X),cons(Y)) -> cons(Y)
from(X) -> cons(X)
Qed